Diagram Chase in Relational System Development

We propose diagrammatic techniques for visualizing relational reasoning in formal methods like B or Z; in particular for induction and coinduction. These are similar to those for functional diagrams in category theory and inspired by rewriting theory. Diagrams are endowed with a simple algebraic semantics that imposes a convenient balance between expressive and algorithmic power. This makes the approach particularly suitable for mechanization and automation. Its usefulness for visual reasoning is illustrated by various examples.     

A framework for specifying and verifying the behaviour of open systems

Coding no longer represents the main issue in developing software applications. It is the design and verification of complex software systems that require to be addressed at the architectural level, following methodologies which permit us to clearly identify and design the components of a system, to understand precisely their interactions, and to formally verify the properties of the systems. Moreover, this process is made even more complicated by the advent of the “network-centric” model of computation, where open systems dynamically interact with each other in a highly volatile environment. Many of the techniques traditionally used for closed systems are inadequate in this context.We illustrate how the problem of modeling and verifying behavioural properties of open system is addressed by different research fields and how their results may contribute to a common solution. Building on this, we propose a methodology for modeling and verifying behavioural aspects of open systems. We introduce the IP-calculus, derived from the π-calculas process algebra so as to describe behavioural features of open systems. We define a notion of partial correctness, acceptability, in order to deal with the intrinsic indeterminacy of open systems, and we provide an algorithmic procedure for its effective verification.     

Towards a probability theory based on Moisil logic

 In this paper a concept of probability defined on a Lukasiewicz-Moisil algebra is proposed. We take some steps in developing the theory, including an extension theorem and some results related to conditional probabilities on Lukasiewicz-Moisil algebras.     

Bio-PEPA: An Extension of the Process Algebra PEPA for Biochemical Networks

In this work we introduce Bio-PEPA, a process algebra for the modelling and the analysis of biochemical networks. It is a modification of PEPA to deal with some features of biological models, such as stoichiometry and the use of generic kinetic laws. Bio-PEPA may be seen as an intermediate, formal, compositional representation of biological systems, on which different kinds of analysis can be carried out. Finally, we show a representation of a model, concerning a simple genetic network, in the new language.     

Extending statecharts with process algebra operators

This paper describes an adaptation of statecharts to take advantage of process algebra operators like those found in CSP and EB³. The resulting notation is called algebraic state transition diagrams (ASTDs). The process algebra operators considered include sequence, iteration, parallel composition, and quantified synchronization. Quantification is one of the salient features of ASTDs, because it provides a powerful mechanism to precisely and explicitly define cardinalities in a dynamic model. The formal semantics of ASTDs is expressed using the operational style typically used in process algebras. The target application domain is the specification and implementation of information systems.     

BR0代数的模糊理想与直觉模糊理想

引入BR₀代数的Fuzzy理想与素Fuzzy理想的概念;给出了Fuzzy理想与素Fuzzy理想的等价形式;在（素）Fuzzy理想基础之上又进一步引入了（素）直觉Fuzzy理想,并通过Fuzzy理想找到了它们与（素）理想之间的关系。     

Using bisimulation proof techniques for the analysis of distributed abstract machines

We illustrate the use of recently developed proof techniques for weak bisimulation by analysing a generic framework for the definition of distributed abstract machines based on a message-passing implementation. We first define this framework, and then focus on the algorithm which is used to route messages asynchronously to their destination.A first version of this algorithm can be analysed using the standard bisimulation up to expansion proof technique. We show that in a second, optimised version, rather complex behaviours appear, for which more sophisticated techniques, relying on termination arguments, are necessary to establish behavioural equivalence.     

BR_0代数的模糊理想与直觉模糊理想

引入BR0代数的Fuzzy理想与素Fuzzy理想的概念;给出了Fuzzy理想与素Fuzzy理想的等价形式;在(素)Fuzzy理想基础之上又进一步引入了(素)直觉Fuzzy理想,并通过Fuzzy理想找到了它们与(素)理想之间的关系。     

Hom-Leibniz代数的直和

定义两个Hom-Leibniz代数(g,[,],α)和(h,[,],β)的直和(gh,[,],α+β),定义两个Hom-Leibniz代数(g,[,],α)和(h,[,],β)的同态Ф,讨论两个Hom-Leibniz代数(g,[,],α)和(h,[,],β)的线性映射Ф成为同态的充分必要条件.     

THEORY OF CYBERNETIC AND INTELLIGENT MACHINE BASED ON LIE COMMUTATORS

Many attempts^{1, 7, 8, 35} have been made to overcome the limit imposed by the Turing Machine³⁴ to realise general mathematical functions and models of (physical) phenomena.

They center around the notion of computability.

In this paper we propose a new definition of computability which lays the foundations for a theory of cybernetic and intelligent machines in which the classical limits imposed by discrete algorithmic procedures are offset by the use of continuous operators on unlimited data. This data is supplied to the machine in a totally parallel mode, as a field or wave.

This theory of machines draws its concepts from category theory, Lie algebras, and general systems theory. It permits the incorporation of intelligent control into the design of the machine as a virtual element. The incorporated control can be realized in many (machine) configurations of which we give three:

a) a quantum mechanical realization appropriate to a possible understanding of the quantum computer and other models of the physical microworld,

b) a stochastic realization based on Kolmogorov-Gabor theory leading to a possible understanding of generalised models of the physical or thermodynamic macroworld, and lastly

c) a classical mechanical realization appropriate lo the study of a new class of robots.

Particular applications at a fundamental level are cited in geometry, mathematics, biology, acoustics, aeronautics, quantum mechanics, general relativity and. Markov chains. The proposed theory therefore opens a new way towards understanding the processes that underlie intelligence.